nLab Bas Spitters

Bas Spitters is professor for formal logic and computer science at Aarhus University and leader of the Concordium Blockchain Research Center

• website

• Concordium page

 Selected writings

On constructive integration theory:

• Bas Spitters, Constructive algebraic integration theory, Annals of Pure and Applied Logic, Volume 137, Issues 1–3, January 2006, Pages 380-390 (pdf, doi:10.1016/j.apal.2005.05.031)

• Bas Spitters, Constructive algebraic integration theory without choice. In Thierry Coquand, Henri Lombardi, Marie-Francoise Roy, Mathematics, Algorithms, Proofs, 2005, Dagstuhl Seminar Proceedings 05021, Internationales Begegnungs- und Forschungszentrum (IBFI), Schloss Dagstuhl, Germany. (pdf)

On constructive analysis with exact real numbers via type theory:

• Herman Geuvers, Milad Niqui, Bas Spitters, Freek Wiedijk, Constructive analysis, types and exact real numbers, Mathematical Structures in Computer Science 17 01 (2007) 3-36 [doi:10.1017/S0960129506005834]

and specifically with Type classes in Coq:

• Robbert Krebbers, Bas Spitters, Type classes for efficient exact real arithmetic in Coq, Logical Methods in Computer Science, 9 1 (2013) lmcs:958 [arXiv:1106.3448, doi:10.2168/LMCS-9(1:1)2013]

Exposition:

• Bas Spitters, Verified Implementation of Exact Real Arithmetic in Type Theory, talk at Computable Analysis and Rigorous Numeric (2013) [pdf, pdf]

On Bohr toposes:

• Chris Heunen, Klaas Landsman, Bas Spitters, Bohrification of operator algebras and quantum logic, Synthese 186 3 (2012) 719-752 [arXiv:0905.2275, doi;10.1007/s11229-011-9918-4]

On mathematical structures formulated in dependent type theory, specifically via Type classes in Coq:

• Bas Spitters, Eelis van der Wegen Type classes for mathematics in type theory, Mathematical Structures in Computer Science 21 4 “Interactive Theorem Proving and the Formalisation of Mathematics” (2011) 795-825 [doi:10.1017/S0960129511000119]

On modalities in homotopy type theory (modal homotopy type theory):

• Egbert Rijke, Mike Shulman, Bas Spitters, Modalities in homotopy type theory, Logical Methods in Computer Science, 16 1 (2020) [arXiv:1706.07526, episciences:6015, doi:10.23638/LMCS-16(1:2)2020]

On software verification for blockchain-technology:

• Bas Spitters, Formal verificaton at Concordium Blockchain Research Center

• Søren Eller Thomsen, Bas Spitters, Formalizing Nakamoto-Style Proof of Stake [eprint:2020/917]

category: people